Formal Analysis of Future Energy Systems Using Interactive Theorem Proving by Asad Ahmed & Osman Hasan & Falah Awwad & Nabil Bastaki

Author:Asad Ahmed & Osman Hasan & Falah Awwad & Nabil Bastaki
Language: eng
Format: epub
ISBN: 9783030784096
Publisher: Springer International Publishing

3.1 Introduction

In this chapter, we present a formalization for the stability analysis of linear time-invariant control systems, represented by characteristic equations of order upto four, with minimal dependence on conventional analysis techniques. We consider complex polynomials with real coefficients, for the purpose of formal analysis in higher-order logic, which allow us to express the cubic and quartic complex polynomials in terms of the quadratic polynomials. However, this choice does not limit the scope of the applicability of our formalization, as these coefficients are usually real numbers as they represent the different parameters of the system, e.g., resistance in electrical and electronics systems. The formally verified roots, which are poles of the system, are then formally analyzed to check for the stability condition, i.e., if they lie in the left-half of the complex-plane, in the sound core of the higher-order-logic theorem prover HOL Light [1]. The main motivation of this choice is the extensive reasoning support available in HOL Light about multivariate complex, real and transcendental theories, which are required for the formalization of stability analysis of control systems.

The rest of the chapter is organized as follows: In Sect. 3.2, we present a review of the related work. This is followed by the description of the proposed methodology about stability analysis in Sect. 3.3. The formalization of the quadratic, cubic and quartic characteristic polynomials is described in Sect. 3.4. We utilize this formalization to formally verify voltage and current controllers designed for the power converters for reliable and efficient smart grid operation in Sect. 3.5. Finally, Sect. 3.6 concludes the chapter.

Download

Copyright Disclaimer:
This site does not store any files on its server. We only index and link to content provided by other sites. Please contact the content providers to delete copyright contents if any and email us, we'll remove relevant links or contents immediately.